MAYBE 2.128
H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/Monad.hs
H-Termination of the given Haskell-Program with start terms could not be shown:
↳ HASKELL
↳ LR
mainModule Monad
| ((mapAndUnzipM :: (a -> [(b,c)]) -> [a] -> [([b],[c])]) :: (a -> [(b,c)]) -> [a] -> [([b],[c])]) |
module Monad where
| import qualified Maybe import qualified Prelude
|
| mapAndUnzipM :: Monad b => (a -> b (d,c)) -> [a] -> b ([d],[c])
mapAndUnzipM | f xs | = | sequence (map f xs) >>= return . unzip |
|
module Maybe where
| import qualified Monad import qualified Prelude
|
Lambda Reductions:
The following Lambda expression
\(a,b)~(as,bs)→(a : as,b : bs)
is transformed to
unzip0 | (a,b) ~(as,bs) | = (a : as,b : bs) |
The following Lambda expression
\xs→return (x : xs)
is transformed to
sequence0 | x xs | = return (x : xs) |
The following Lambda expression
\x→sequence cs >>= sequence0 x
is transformed to
sequence1 | cs x | = sequence cs >>= sequence0 x |
↳ HASKELL
↳ LR
↳ HASKELL
↳ IPR
mainModule Monad
| ((mapAndUnzipM :: (c -> [(b,a)]) -> [c] -> [([b],[a])]) :: (c -> [(b,a)]) -> [c] -> [([b],[a])]) |
module Maybe where
| import qualified Monad import qualified Prelude
|
module Monad where
| import qualified Maybe import qualified Prelude
|
| mapAndUnzipM :: Monad b => (d -> b (a,c)) -> [d] -> b ([a],[c])
mapAndUnzipM | f xs | = | sequence (map f xs) >>= return . unzip |
|
IrrPat Reductions:
The variables of the following irrefutable Pattern
~(as,bs)
are replaced by calls to these functions
↳ HASKELL
↳ LR
↳ HASKELL
↳ IPR
↳ HASKELL
↳ BR
mainModule Monad
| ((mapAndUnzipM :: (a -> [(c,b)]) -> [a] -> [([c],[b])]) :: (a -> [(c,b)]) -> [a] -> [([c],[b])]) |
module Monad where
| import qualified Maybe import qualified Prelude
|
| mapAndUnzipM :: Monad c => (d -> c (a,b)) -> [d] -> c ([a],[b])
mapAndUnzipM | f xs | = | sequence (map f xs) >>= return . unzip |
|
module Maybe where
| import qualified Monad import qualified Prelude
|
Replaced joker patterns by fresh variables and removed binding patterns.
↳ HASKELL
↳ LR
↳ HASKELL
↳ IPR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
mainModule Monad
| ((mapAndUnzipM :: (c -> [(b,a)]) -> [c] -> [([b],[a])]) :: (c -> [(b,a)]) -> [c] -> [([b],[a])]) |
module Maybe where
| import qualified Monad import qualified Prelude
|
module Monad where
| import qualified Maybe import qualified Prelude
|
| mapAndUnzipM :: Monad c => (a -> c (b,d)) -> [a] -> c ([b],[d])
mapAndUnzipM | f xs | = | sequence (map f xs) >>= return . unzip |
|
Cond Reductions:
The following Function with conditions
is transformed to
undefined0 | True | = undefined |
undefined1 | | = undefined0 False |
↳ HASKELL
↳ LR
↳ HASKELL
↳ IPR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ Narrow
mainModule Monad
| (mapAndUnzipM :: (a -> [(c,b)]) -> [a] -> [([c],[b])]) |
module Monad where
| import qualified Maybe import qualified Prelude
|
| mapAndUnzipM :: Monad c => (b -> c (d,a)) -> [b] -> c ([d],[a])
mapAndUnzipM | f xs | = | sequence (map f xs) >>= return . unzip |
|
module Maybe where
| import qualified Monad import qualified Prelude
|
Haskell To QDPs
↳ HASKELL
↳ LR
↳ HASKELL
↳ IPR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ Narrow
Q DP problem:
The TRS P consists of the following rules:
new_gtGtEs(:(vz280, vz281), vz71, vz50, h, ba) → new_gtGtEs(vz281, vz71, vz50, h, ba)
new_gtGtEs([], :(vz710, vz711), vz50, h, ba) → new_gtGtEs(new_psPs(vz710, [], new_gtGtEs0(vz710, h, ba), h, ba), vz711, vz50, h, ba)
The TRS R consists of the following rules:
new_gtGtEs0(vz50, h, ba) → []
new_psPs(vz50, vz230, vz27, h, ba) → :(:(vz50, vz230), vz27)
The set Q consists of the following terms:
new_gtGtEs0(x0, x1, x2)
new_psPs(x0, x1, x2, x3, x4)
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_gtGtEs(:(vz280, vz281), vz71, vz50, h, ba) → new_gtGtEs(vz281, vz71, vz50, h, ba)
The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3, 4 >= 4, 5 >= 5
- new_gtGtEs([], :(vz710, vz711), vz50, h, ba) → new_gtGtEs(new_psPs(vz710, [], new_gtGtEs0(vz710, h, ba), h, ba), vz711, vz50, h, ba)
The graph contains the following edges 2 > 2, 3 >= 3, 4 >= 4, 5 >= 5
↳ HASKELL
↳ LR
↳ HASKELL
↳ IPR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ Narrow
Q DP problem:
The TRS P consists of the following rules:
new_gtGtEs1([], :(vz710, vz711), vz160, vz161, vz50, h, ba) → new_gtGtEs1(new_sequence1(vz160, vz161, vz710, h, ba), vz711, vz160, vz161, vz50, h, ba)
new_gtGtEs1(:(vz240, vz241), vz71, vz160, vz161, vz50, h, ba) → new_gtGtEs1(vz241, vz71, vz160, vz161, vz50, h, ba)
The TRS R consists of the following rules:
new_gtGtEs4([], [], vz50, h, ba) → new_gtGtEs0(vz50, h, ba)
new_sequence1(vz20, vz21, vz190, bb, bc) → new_gtGtEs2(vz20, vz21, vz190, bb, bc)
new_gtGtEs2(vz70, vz71, vz50, h, ba) → new_psPs(vz50, :(vz70, []), new_gtGtEs3(new_gtGtEs0(vz70, h, ba), vz71, vz50, h, ba), h, ba)
new_gtGtEs0(vz50, h, ba) → []
new_gtGtEs3(vz28, vz71, vz50, h, ba) → new_gtGtEs4(vz28, vz71, vz50, h, ba)
new_gtGtEs4(:(vz280, vz281), vz71, vz50, h, ba) → new_psPs(vz50, vz280, new_gtGtEs4(vz281, vz71, vz50, h, ba), h, ba)
new_psPs(vz50, vz230, vz27, h, ba) → :(:(vz50, vz230), vz27)
new_gtGtEs4([], :(vz710, vz711), vz50, h, ba) → new_gtGtEs4(new_psPs(vz710, [], new_gtGtEs0(vz710, h, ba), h, ba), vz711, vz50, h, ba)
The set Q consists of the following terms:
new_gtGtEs2(x0, x1, x2, x3, x4)
new_gtGtEs0(x0, x1, x2)
new_gtGtEs3(x0, x1, x2, x3, x4)
new_sequence1(x0, x1, x2, x3, x4)
new_psPs(x0, x1, x2, x3, x4)
new_gtGtEs4([], [], x0, x1, x2)
new_gtGtEs4([], :(x0, x1), x2, x3, x4)
new_gtGtEs4(:(x0, x1), x2, x3, x4, x5)
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_gtGtEs1([], :(vz710, vz711), vz160, vz161, vz50, h, ba) → new_gtGtEs1(new_sequence1(vz160, vz161, vz710, h, ba), vz711, vz160, vz161, vz50, h, ba)
The graph contains the following edges 2 > 2, 3 >= 3, 4 >= 4, 5 >= 5, 6 >= 6, 7 >= 7
- new_gtGtEs1(:(vz240, vz241), vz71, vz160, vz161, vz50, h, ba) → new_gtGtEs1(vz241, vz71, vz160, vz161, vz50, h, ba)
The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3, 4 >= 4, 5 >= 5, 6 >= 6, 7 >= 7
↳ HASKELL
↳ LR
↳ HASKELL
↳ IPR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ Narrow
Q DP problem:
The TRS P consists of the following rules:
new_gtGtEs7(vz3, vz41110, vz41111, h, ba, bb) → new_gtGtEs7(vz3, vz41110, vz41111, h, ba, bb)
new_gtGtEs6(vz3, :(vz41110, vz41111), h, ba, bb) → new_gtGtEs7(vz3, vz41110, vz41111, h, ba, bb)
new_gtGtEs6(vz3, :(vz41110, vz41111), h, ba, bb) → new_gtGtEs5(vz3, vz41110, vz41111, h, ba, bb)
new_gtGtEs6(vz3, vz4111, h, ba, bb) → new_gtGtEs6(vz3, vz4111, h, ba, bb)
new_sequence11(vz13, vz14, vz15, bc, bd, be) → new_gtGtEs5(vz13, vz14, vz15, bc, bd, be)
new_gtGtEs5(vz3, vz4110, vz4111, h, ba, bb) → new_gtGtEs6(vz3, vz4111, h, ba, bb)
new_gtGtEs7(vz3, vz41110, vz41111, h, ba, bb) → new_sequence11(vz3, vz41110, vz41111, h, ba, bb)
The TRS R consists of the following rules:
new_sequence10(vz11, vz12, vz13, vz14, vz15, vz100, bc, bd, be) → new_gtGtEs8(vz13, vz14, vz15, vz11, vz12, vz100, bc, bd, be)
The set Q consists of the following terms:
new_sequence10(x0, x1, x2, x3, x4, x5, x6, x7, x8)
We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.
↳ HASKELL
↳ LR
↳ HASKELL
↳ IPR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ Narrow
Q DP problem:
The TRS P consists of the following rules:
new_gtGtEs7(vz3, vz41110, vz41111, h, ba, bb) → new_gtGtEs7(vz3, vz41110, vz41111, h, ba, bb)
new_gtGtEs6(vz3, :(vz41110, vz41111), h, ba, bb) → new_gtGtEs7(vz3, vz41110, vz41111, h, ba, bb)
new_gtGtEs6(vz3, :(vz41110, vz41111), h, ba, bb) → new_gtGtEs5(vz3, vz41110, vz41111, h, ba, bb)
new_gtGtEs6(vz3, vz4111, h, ba, bb) → new_gtGtEs6(vz3, vz4111, h, ba, bb)
new_sequence11(vz13, vz14, vz15, bc, bd, be) → new_gtGtEs5(vz13, vz14, vz15, bc, bd, be)
new_gtGtEs5(vz3, vz4110, vz4111, h, ba, bb) → new_gtGtEs6(vz3, vz4111, h, ba, bb)
new_gtGtEs7(vz3, vz41110, vz41111, h, ba, bb) → new_sequence11(vz3, vz41110, vz41111, h, ba, bb)
R is empty.
The set Q consists of the following terms:
new_sequence10(x0, x1, x2, x3, x4, x5, x6, x7, x8)
We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.
new_sequence10(x0, x1, x2, x3, x4, x5, x6, x7, x8)
↳ HASKELL
↳ LR
↳ HASKELL
↳ IPR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ UsableRulesReductionPairsProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ Narrow
Q DP problem:
The TRS P consists of the following rules:
new_gtGtEs7(vz3, vz41110, vz41111, h, ba, bb) → new_gtGtEs7(vz3, vz41110, vz41111, h, ba, bb)
new_gtGtEs6(vz3, :(vz41110, vz41111), h, ba, bb) → new_gtGtEs5(vz3, vz41110, vz41111, h, ba, bb)
new_gtGtEs6(vz3, :(vz41110, vz41111), h, ba, bb) → new_gtGtEs7(vz3, vz41110, vz41111, h, ba, bb)
new_sequence11(vz13, vz14, vz15, bc, bd, be) → new_gtGtEs5(vz13, vz14, vz15, bc, bd, be)
new_gtGtEs6(vz3, vz4111, h, ba, bb) → new_gtGtEs6(vz3, vz4111, h, ba, bb)
new_gtGtEs5(vz3, vz4110, vz4111, h, ba, bb) → new_gtGtEs6(vz3, vz4111, h, ba, bb)
new_gtGtEs7(vz3, vz41110, vz41111, h, ba, bb) → new_sequence11(vz3, vz41110, vz41111, h, ba, bb)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the usable rules with reduction pair processor [15] with a polynomial ordering [25], all dependency pairs and the corresponding usable rules [17] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.
The following dependency pairs can be deleted:
new_gtGtEs6(vz3, :(vz41110, vz41111), h, ba, bb) → new_gtGtEs5(vz3, vz41110, vz41111, h, ba, bb)
new_gtGtEs6(vz3, :(vz41110, vz41111), h, ba, bb) → new_gtGtEs7(vz3, vz41110, vz41111, h, ba, bb)
new_gtGtEs7(vz3, vz41110, vz41111, h, ba, bb) → new_sequence11(vz3, vz41110, vz41111, h, ba, bb)
No rules are removed from R.
Used ordering: POLO with Polynomial interpretation [25]:
POL(:(x1, x2)) = 1 + 2·x1 + x2
POL(new_gtGtEs5(x1, x2, x3, x4, x5, x6)) = x1 + x2 + 2·x3 + x4 + x5 + x6
POL(new_gtGtEs6(x1, x2, x3, x4, x5)) = x1 + 2·x2 + x3 + x4 + x5
POL(new_gtGtEs7(x1, x2, x3, x4, x5, x6)) = 1 + x1 + 2·x2 + 2·x3 + x4 + x5 + x6
POL(new_sequence11(x1, x2, x3, x4, x5, x6)) = x1 + 2·x2 + 2·x3 + x4 + x5 + x6
↳ HASKELL
↳ LR
↳ HASKELL
↳ IPR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ UsableRulesReductionPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ Narrow
Q DP problem:
The TRS P consists of the following rules:
new_gtGtEs7(vz3, vz41110, vz41111, h, ba, bb) → new_gtGtEs7(vz3, vz41110, vz41111, h, ba, bb)
new_gtGtEs6(vz3, vz4111, h, ba, bb) → new_gtGtEs6(vz3, vz4111, h, ba, bb)
new_sequence11(vz13, vz14, vz15, bc, bd, be) → new_gtGtEs5(vz13, vz14, vz15, bc, bd, be)
new_gtGtEs5(vz3, vz4110, vz4111, h, ba, bb) → new_gtGtEs6(vz3, vz4111, h, ba, bb)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs with 2 less nodes.
↳ HASKELL
↳ LR
↳ HASKELL
↳ IPR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ UsableRulesReductionPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ NonTerminationProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ Narrow
Q DP problem:
The TRS P consists of the following rules:
new_gtGtEs6(vz3, vz4111, h, ba, bb) → new_gtGtEs6(vz3, vz4111, h, ba, bb)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.
The TRS P consists of the following rules:
new_gtGtEs6(vz3, vz4111, h, ba, bb) → new_gtGtEs6(vz3, vz4111, h, ba, bb)
The TRS R consists of the following rules:none
s = new_gtGtEs6(vz3, vz4111, h, ba, bb) evaluates to t =new_gtGtEs6(vz3, vz4111, h, ba, bb)
Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
- Semiunifier: [ ]
- Matcher: [ ]
Rewriting sequence
The DP semiunifies directly so there is only one rewrite step from new_gtGtEs6(vz3, vz4111, h, ba, bb) to new_gtGtEs6(vz3, vz4111, h, ba, bb).
↳ HASKELL
↳ LR
↳ HASKELL
↳ IPR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ UsableRulesReductionPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ NonTerminationProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ Narrow
Q DP problem:
The TRS P consists of the following rules:
new_gtGtEs7(vz3, vz41110, vz41111, h, ba, bb) → new_gtGtEs7(vz3, vz41110, vz41111, h, ba, bb)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.
The TRS P consists of the following rules:
new_gtGtEs7(vz3, vz41110, vz41111, h, ba, bb) → new_gtGtEs7(vz3, vz41110, vz41111, h, ba, bb)
The TRS R consists of the following rules:none
s = new_gtGtEs7(vz3, vz41110, vz41111, h, ba, bb) evaluates to t =new_gtGtEs7(vz3, vz41110, vz41111, h, ba, bb)
Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
- Semiunifier: [ ]
- Matcher: [ ]
Rewriting sequence
The DP semiunifies directly so there is only one rewrite step from new_gtGtEs7(vz3, vz41110, vz41111, h, ba, bb) to new_gtGtEs7(vz3, vz41110, vz41111, h, ba, bb).
↳ HASKELL
↳ LR
↳ HASKELL
↳ IPR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ Narrow
Q DP problem:
The TRS P consists of the following rules:
new_foldr(:(vz900, vz901), h, ba) → new_foldr(vz901, h, ba)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_foldr(:(vz900, vz901), h, ba) → new_foldr(vz901, h, ba)
The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3
↳ HASKELL
↳ LR
↳ HASKELL
↳ IPR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ Narrow
Q DP problem:
The TRS P consists of the following rules:
new_gtGtEs9(vz50, :(vz510, vz511), h, ba) → new_gtGtEs9(vz510, vz511, h, ba)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_gtGtEs9(vz50, :(vz510, vz511), h, ba) → new_gtGtEs9(vz510, vz511, h, ba)
The graph contains the following edges 2 > 1, 2 > 2, 3 >= 3, 4 >= 4
↳ HASKELL
↳ LR
↳ HASKELL
↳ IPR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ Narrow
Q DP problem:
The TRS P consists of the following rules:
new_gtGtEs10([], :(vz190, vz191), vz20, vz21, h, ba) → new_gtGtEs10(new_sequence1(vz20, vz21, vz190, h, ba), vz191, vz20, vz21, h, ba)
new_gtGtEs10(:(vz180, vz181), vz19, vz20, vz21, h, ba) → new_gtGtEs10(vz181, vz19, vz20, vz21, h, ba)
The TRS R consists of the following rules:
new_gtGtEs4([], [], vz50, bb, bc) → new_gtGtEs0(vz50, bb, bc)
new_sequence1(vz20, vz21, vz190, h, ba) → new_gtGtEs2(vz20, vz21, vz190, h, ba)
new_gtGtEs2(vz70, vz71, vz50, bb, bc) → new_psPs(vz50, :(vz70, []), new_gtGtEs3(new_gtGtEs0(vz70, bb, bc), vz71, vz50, bb, bc), bb, bc)
new_gtGtEs0(vz50, bb, bc) → []
new_gtGtEs3(vz28, vz71, vz50, bb, bc) → new_gtGtEs4(vz28, vz71, vz50, bb, bc)
new_gtGtEs4(:(vz280, vz281), vz71, vz50, bb, bc) → new_psPs(vz50, vz280, new_gtGtEs4(vz281, vz71, vz50, bb, bc), bb, bc)
new_psPs(vz50, vz230, vz27, bb, bc) → :(:(vz50, vz230), vz27)
new_gtGtEs4([], :(vz710, vz711), vz50, bb, bc) → new_gtGtEs4(new_psPs(vz710, [], new_gtGtEs0(vz710, bb, bc), bb, bc), vz711, vz50, bb, bc)
The set Q consists of the following terms:
new_gtGtEs2(x0, x1, x2, x3, x4)
new_gtGtEs3(x0, x1, x2, x3, x4)
new_gtGtEs4(:(x0, x1), x2, x3, x4, x5)
new_gtGtEs0(x0, x1, x2)
new_sequence1(x0, x1, x2, x3, x4)
new_gtGtEs4([], :(x0, x1), x2, x3, x4)
new_psPs(x0, x1, x2, x3, x4)
new_gtGtEs4([], [], x0, x1, x2)
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_gtGtEs10([], :(vz190, vz191), vz20, vz21, h, ba) → new_gtGtEs10(new_sequence1(vz20, vz21, vz190, h, ba), vz191, vz20, vz21, h, ba)
The graph contains the following edges 2 > 2, 3 >= 3, 4 >= 4, 5 >= 5, 6 >= 6
- new_gtGtEs10(:(vz180, vz181), vz19, vz20, vz21, h, ba) → new_gtGtEs10(vz181, vz19, vz20, vz21, h, ba)
The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3, 4 >= 4, 5 >= 5, 6 >= 6
↳ HASKELL
↳ LR
↳ HASKELL
↳ IPR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrow
Q DP problem:
The TRS P consists of the following rules:
new_gtGtEs11(:(vz90, vz91), vz10, vz11, vz12, vz13, vz14, vz15, h, ba, bb) → new_gtGtEs11(vz91, vz10, vz11, vz12, vz13, vz14, vz15, h, ba, bb)
new_gtGtEs11([], :(vz100, vz101), vz11, vz12, vz13, vz14, vz15, h, ba, bb) → new_gtGtEs11(new_sequence10(vz11, vz12, vz13, vz14, vz15, vz100, h, ba, bb), vz101, vz11, vz12, vz13, vz14, vz15, h, ba, bb)
The TRS R consists of the following rules:
new_sequence10(vz11, vz12, vz13, vz14, vz15, vz100, h, ba, bb) → new_gtGtEs8(vz13, vz14, vz15, vz11, vz12, vz100, h, ba, bb)
The set Q consists of the following terms:
new_sequence10(x0, x1, x2, x3, x4, x5, x6, x7, x8)
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.
↳ HASKELL
↳ LR
↳ HASKELL
↳ IPR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Narrow
Q DP problem:
The TRS P consists of the following rules:
new_gtGtEs11(:(vz90, vz91), vz10, vz11, vz12, vz13, vz14, vz15, h, ba, bb) → new_gtGtEs11(vz91, vz10, vz11, vz12, vz13, vz14, vz15, h, ba, bb)
The TRS R consists of the following rules:
new_sequence10(vz11, vz12, vz13, vz14, vz15, vz100, h, ba, bb) → new_gtGtEs8(vz13, vz14, vz15, vz11, vz12, vz100, h, ba, bb)
The set Q consists of the following terms:
new_sequence10(x0, x1, x2, x3, x4, x5, x6, x7, x8)
We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.
↳ HASKELL
↳ LR
↳ HASKELL
↳ IPR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrow
Q DP problem:
The TRS P consists of the following rules:
new_gtGtEs11(:(vz90, vz91), vz10, vz11, vz12, vz13, vz14, vz15, h, ba, bb) → new_gtGtEs11(vz91, vz10, vz11, vz12, vz13, vz14, vz15, h, ba, bb)
R is empty.
The set Q consists of the following terms:
new_sequence10(x0, x1, x2, x3, x4, x5, x6, x7, x8)
We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.
new_sequence10(x0, x1, x2, x3, x4, x5, x6, x7, x8)
↳ HASKELL
↳ LR
↳ HASKELL
↳ IPR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ Narrow
Q DP problem:
The TRS P consists of the following rules:
new_gtGtEs11(:(vz90, vz91), vz10, vz11, vz12, vz13, vz14, vz15, h, ba, bb) → new_gtGtEs11(vz91, vz10, vz11, vz12, vz13, vz14, vz15, h, ba, bb)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_gtGtEs11(:(vz90, vz91), vz10, vz11, vz12, vz13, vz14, vz15, h, ba, bb) → new_gtGtEs11(vz91, vz10, vz11, vz12, vz13, vz14, vz15, h, ba, bb)
The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3, 4 >= 4, 5 >= 5, 6 >= 6, 7 >= 7, 8 >= 8, 9 >= 9, 10 >= 10
↳ HASKELL
↳ LR
↳ HASKELL
↳ IPR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ Narrow
Q DP problem:
The TRS P consists of the following rules:
new_gtGtEs12([], vz3, vz411, vz50, :(vz510, vz511), h, ba, bb) → new_gtGtEs12([], vz3, vz411, vz510, vz511, h, ba, bb)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_gtGtEs12([], vz3, vz411, vz50, :(vz510, vz511), h, ba, bb) → new_gtGtEs12([], vz3, vz411, vz510, vz511, h, ba, bb)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 5 > 4, 5 > 5, 6 >= 6, 7 >= 7, 8 >= 8
Haskell To QDPs